The present invention relates generally to model checking, which is an automated approach to proving properties about programs through exhaustive state space exploration. More particularly, the present invention relates to a preprocessing method and system for model-checking languages which can be used to improve performance of model checking tools.
Model checking (both explicit state and symbolic) has been successfully used to verify properties of various finite state systems, such as communications protocols, concurrent systems, hardware designs, and software systems. The primary limitation of model checking is the state space explosion problem, which limits the size of systems that can be successfully checked by a model checker.
For implicit state model checkers, the state space is not explicitly represented; instead, sets of states, and the model itself, are described as a formula over a set of Boolean variables. For these tools, it is not only the number of reachable states but also the size of the Boolean representation of the state and the model that determine whether or not a tool is able to successfully analyze the model.
For implicit state model checking tools, it is well known that the structure of the Boolean formula representing the model affects the difficulty of verifying properties over it, and a considerable amount of research has been done to try to minimize the size of the Boolean representation of a model. Many checkers, such as the Symbolic Model Verifier (SMV) available from Carnegie Mellon University and the Symbolic Analysis Laboratory (SAL) available from Stanford Research Institute (SRI) Inc. are based on Binary Decision Diagram (BDD) representations of Boolean formulae. BDDs provide a compact, efficient encoding of Boolean formulae. The performance of logical operations on BDDs, and therefore model checking tools based on BDDs, is sensitive both to the number of variables necessary to encode the model and also to the ordering of variables within the BDD.